FDL - Step of Proof: p-restrict_wf

Step of Proof: p-restrict_wf

Inference at *
Iof proof for Lemma p-restrict wf:

A, B:Type, f:(A

(B + Top)), P:(A

), p:(

x:A. Dec(P(x))). p-restrict(f;p)

A

(B + Top)

by ((Unfold `p-restrict` 0)
CollapseTHEN (Auto

))

Co.

Definitions p-restrict(f;p), f o g , p-filter(f), x. t(x), x.A(x), Dec(P), x:A. B(x), x(s), f(a), , x:AB(x), left + right, Top, t T, Type

Lemmas p-compose wf, p-filter wf, decidable wf, top wf